test: attack eighteen arms across three parts (#1236) - #1246
Conversation
jdatcmd
left a comment
There was a problem hiding this comment.
Approving 52fd3e82. Derived from the artifact; the one claim I set out to break survives.
The 18-versus-15 gap is real and is the finding, not an error
rows changed 18
of those, never -> dated 15
already dated, date and cause advanced 3
the nulls column fetched by index matches the heap, row 2026-09-18
the nulls column holds no row the heap does not 2026-09-18
the nulls column reads back exactly what the heap holds 2026-09-18
dated -> never 0
census 1606 rows, 1497 never, 109 not-never, 1497 + 109 == 1606, budget agrees
and 1512 - 15 = 1497
Three validity_elision arms were already dated under the inverse mutation — the elision predicate forced false where this forces it true — and pgc_ledger accumulated both strings rather than overwriting. Flagging that before I derived it was the right call: 15 where the body says 18 reads as an error until you know which quantity each is.
The disjointness claim, which is the half I attacked
b190A "never asks for a clean" 5 arms
b190C "always demands a clean" 2 arms
intersection 0
The five are the ones that demand a clean; the two are building the same major again needs no clean and but a tree with no objects at all needs nothing, stamp or not. Forcing the decision one way reddens one set and leaves the other green; forcing it the other way swaps them exactly. A single mutation cannot establish that — it takes the pair, and the pair is what shows the arms measure the DECISION rather than a side effect of it.
And the enumeration holds. I went looking for a sixteenth arm, because that is what would break the claim that only those two separate a correct guard from a merely fail-closed one:
sed strip | grep -cE '^[[:space:]]*check' 15
unstripped, same pattern 15
strip | grep -cE '^[[:space:]]*check(_num|_text)? "' 15
ledger rows for part 190 15
No sixteenth. So there is no arm that should have reddened under b190C and did not, and the categorisation is exhaustive.
One thing my own attack turned up, in my instrument rather than in this PR. My name extraction found 14 of those 15, because the missing one is
building a DIFFERENT major needs a clean, which is the #536 case
A check NAME containing #536, truncated past its closing quote by comment-stripping. I checked whether the parity tooling shares that blind spot and it does not — _bash_names returns the full string, and the ledger reads RESULT lines from logs rather than names from source. Only ad-hoc extraction is exposed, which is where the counting gets done.
The three still-never arms resolve by reading
premise: the build-stamp decision is exposed to be judged and premise: the stamp writer is a function that can be exercised are type -t calls. a comment naming the call does not satisfy the arm above builds its own one-line fixture and asserts that sed 's/#.*//' strips a comment — a property of sed, not of pgcolumnar. Fixture facts in the strict sense, and the correct answer to "is there a third mutation nobody wrote".
Six mutations over validity_elision, selftest part 190 and native_join_vector_agg. No test changed and no code changed: the arms were attacked and the ledger records what happened. veC the elision predicate forced true 5 arms b190A pgc_build_needs_clean never asks for a clean 5 arms b190B the stamp writes an escaped literal (commandprompt#898) 2 arms b190C pgc_build_needs_clean always demands a clean 2 arms b190D unknown provenance reported as a major, PG? 2 arms jvaB the dim-side uniqueness refusal disabled 2 arms b190A and b190C are opposites and redden disjoint pairs. A guard that never cleans loses the five arms about when a clean is required; one that always cleans loses exactly two, and only those two separate a correct guard from one that is merely fail-closed. Fifteen of the eighteen rows are newly dated. The other three are validity_elision arms already dated under the inverse mutation -- the predicate forced false rather than true -- so they now carry both strings and the later date, rather than the newer observation overwriting the older. Re-derived on the merged tree. All six had run once before commandprompt#1240 and commandprompt#1241 landed and were re-run against ac80762, reproducing their earlier results exactly: same names, not merely the same counts, with a control showing the comparison can separate two unrelated sets. The two C mutations ran with a forced make clean, because PGXS here has no --enable-depend and a stale object after a header edit would leave veC reddening nothing. Census re-derived by counting: 1606 rows, 109 not never, 1497 + 109 == 1606. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01MpajdQbkVJ9ey1XyYHcikP
52fd3e8 to
88f33cf
Compare
jdatcmd
left a comment
There was a problem hiding this comment.
Re-approving on 88f33cfe. My earlier approval was on 52fd3e82 and does not cover this head — the rebase moved the census, and the census is the claim this PR makes.
Re-verified rather than carried:
census 1613 rows, 1496 never, 117 dated, 1496 + 117 == 1613, budget 1496
files CHANGELOG.md, check_ledger.tsv, check_ledger_budget.txt only
per part 400 rows=103 dated=8 190 rows=15 dated=12
validity_elision 13 native_join_vector_agg 8
checks 15 of 15 success, 0 pending, 0 missing, 0 extra vs 8bd737bc
state CLEAN
The per-part counts are the check the totals cannot make. Two sets can sum correctly with one row lost from one side and one duplicated from the other, and the census would still reconcile. Part 400's 103 rows are #1244's, part 190's 12 dated are this PR's, and both survive the auto-merge intact.
1496 was predicted before the rebase and counted after it, by both of us separately. The branch had carried 1497, describing a main without #1244; that number was discarded rather than picked. Neither side's stale figure survived, which is the only correct outcome when two ledger branches meet.
#1236's third, fourth and fifth batches. Eighteen arms attacked across three
parts. No test changed and no code changed — the diff is the ledger rows,
the budget note and the CHANGELOG.
Six mutations, predictions written before they ran
b190A and b190C are opposites and redden disjoint pairs, which is the pair
worth reading. A guard that never cleans loses the five arms about when a
clean is required. A guard that always cleans loses exactly two — "building
the same major again needs no clean" and "but a tree with no objects at all
needs nothing, stamp or not". Only those two separate a correct guard from one
that is merely fail-closed, and a guard cleaning unconditionally would pass
every other arm in the part.
Eighteen rows touched, fifteen newly dated
The other three are
validity_elisionarms already dated 2026-09-18 under theinverse mutation — the elision predicate forced false, so every reader
expects a bitmap the writer did not write. This batch forces it true. Both
directions redden the same three arms, so those rows now carry both mutation
strings and the later date rather than the newer observation overwriting the
older. An arm reddened by a predicate in either direction is better evidence
than one reddened in a single direction.
Re-derived on the merged tree, not carried forward
These six ran once before #1240 and #1241 landed. I re-ran all six against
ac80762arather than merging the logs I had held, and every one reproduced itsearlier result exactly — same names, not merely the same counts:
So the held logs would have served. Re-running is what makes that a measurement
rather than an assumption: "the check names still exist" and "the mutations
still redden them" are different claims, and only re-running tests the second.
I had verified the first in advance, which proves less than it looks like.
Every anchor was dry-run first — apply, assert the digest moved, restore, assert
byte-identical — before a single suite ran.
The two C mutations ran with a forced
make clean. PGXS here has no--enable-depend, so a stale object after a header edit would leaveveCreddening nothing and reading exactly like a fixture fact — a false negative on
the one mutation whose subject is a decode predicate.
Verification
Census re-derived by counting on this tree, not carried:
Note on the reading list
This will push #1236's reading list up, not down, and that is the metric
behaving correctly rather than a regression. The list is "never, non-premise, in
a part where a sibling is dated", so the first attack on a part promotes its
unattacked siblings from invisible to suspect. #1244 did the same thing: 72 to
154, because part 400 went from zero dated arms to eight. Parts-with-a-dated-arm
is the monotone companion number.
🤖 Generated with Claude Code
https://claude.ai/code/session_01MpajdQbkVJ9ey1XyYHcikP